(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
a__dbl(0) → 0
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0, cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(0) → 0
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
a__sel(0, cons(sel(0, cons(X11792_3, X21793_3)), Y)) →+ a__sel(0, cons(X11792_3, X21793_3))
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [X11792_3 / sel(0, cons(X11792_3, X21793_3))].
The result substitution is [Y / X21793_3].
(2) BOUNDS(n^1, INF)
(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
S is empty.
Rewrite Strategy: INNERMOST
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
Innermost TRS:
Rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
hole_0':s:dbl:nil:cons:dbls:sel:indx:from1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from
gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from
(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
a__sel,
markThey will be analysed ascendingly in the following order:
a__sel = mark
(8) Obligation:
Innermost TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
hole_0':s:dbl:nil:cons:dbls:sel:indx:from1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from
gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0(x))
The following defined symbols remain to be analysed:
mark, a__sel
They will be analysed ascendingly in the following order:
a__sel = mark
(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol mark.
(10) Obligation:
Innermost TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
hole_0':s:dbl:nil:cons:dbls:sel:indx:from1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from
gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0(x))
The following defined symbols remain to be analysed:
a__sel
They will be analysed ascendingly in the following order:
a__sel = mark
(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol a__sel.
(12) Obligation:
Innermost TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from → 0':s:dbl:nil:cons:dbls:sel:indx:from
hole_0':s:dbl:nil:cons:dbls:sel:indx:from1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from
gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from2_0(x))
No more defined symbols left to analyse.